\begin{tabbing}
es{-}interface{-}local\=\{i:l\}\+
\\[0ex](${\it es}$; $A$; $X$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=$f$:\=$i$:Id$\rightarrow$${\it xs}$:(Id List)\+\+
\\[0ex]$\times$ ($k$:Knd$\rightarrow$es{-}partial{-}state(${\it es}$;$i$;${\it xs}$)$\rightarrow$es{-}kindtype(${\it es}$;$i$;$k$)$\rightarrow$($A$ + Top))
\-\\[0ex](\=$X$\+
\\[0ex]=
\\[0ex]($\lambda$$e$.(($f$(es{-}loc(${\it es}$; $e$))).2)(es{-}kind(${\it es}$; $e$),es{-}state{-}when(${\it es}$;$e$),es{-}val(${\it es}$; $e$)))
\\[0ex]$\in$ es{-}E(${\it es}$)$\rightarrow$($A$ + Top))
\-\-
\end{tabbing}